Termination Proof Script

Consider the TRS R consisting of the rewrite rule
1:    app(app(*,x),app(app(+,y),z))  → app(app(+,app(app(*,x),y)),app(app(*,x),z))
There are 4 dependency pairs:
2:    APP(app(*,x),app(app(+,y),z))  → APP(app(+,app(app(*,x),y)),app(app(*,x),z))
3:    APP(app(*,x),app(app(+,y),z))  → APP(+,app(app(*,x),y))
4:    APP(app(*,x),app(app(+,y),z))  → APP(app(*,x),y)
5:    APP(app(*,x),app(app(+,y),z))  → APP(app(*,x),z)
The approximated dependency graph contains one SCC: {2,4,5}.
Tyrolean Termination Tool  (0.08 seconds)   ---  May 4, 2006